package kunsch.bdd;

import kunsch.bexp.And;
import kunsch.bexp.Expression;
import kunsch.bexp.False;
import kunsch.bexp.Not;
import kunsch.bexp.Or;
import kunsch.bexp.True;
import kunsch.bexp.Variable;

public class BBDCreator
{
	AbstractBDD bdd;
	int varCount;
	int layer = 0;

	AbstractNode[] lastNodes;
	Boolean[] lastNegated;

	public AbstractBDD transformToBDD(Expression exp, int varCount)
	{
		return transformToBDD(exp, varCount, null);
	}

	public AbstractBDD transformToBDD(Expression exp, int varCount, BDDReduceStrategy reduceStrat)
	{
		this.varCount = varCount;
		this.bdd = new BDD();
		this.lastNodes = new AbstractNode[varCount];
		this.lastNegated = new Boolean[varCount];

		parseExpression(exp);

		if (reduceStrat != null)
			this.bdd = reduceStrat.reduceBdd(bdd);

		return bdd;
	}

	private void parseExpression(Expression exp)
	{

		if (exp instanceof Or)
		{
			for (Expression actExp : ((Or) exp).getExpressions())
			{
				parseExpression(actExp);
			}

		}
		else if (exp instanceof And)
		{
			And and = (And) exp;
			for (int i = 0; i < and.getExpressions().size(); i++)
			{
				if (i == 0)
				{
					parseExpression(and.getExpressions().get(i));
				}
				else
				{
					layer++;
					parseExpression(and.getExpressions().get(i));
					// current layer variable is handled and lastNode is set to
					// Null so a new Variable in the same layer can be created
					// later

					if (lastNodes.length > layer)
						lastNodes[layer] = null;
					layer--;
				}
			}

		}

		else if (exp instanceof Variable)
		{
			if (lastNodes[layer] == null)
			{
				// no current layer variable has been created so create one now
				Node node = new Node("none");
				node.setDescription(((Variable) exp).getDescription());
				lastNodes[layer] = node;
				bdd.addNode(node);
			}

			specialHandling(exp);

			if (exp.getParent() instanceof Not)
				lastNegated[layer] = true;
			else
				lastNegated[layer] = false;

			if (layer > 0)
			{
				// set the correct paths from the upper layer node to the
				// currentNode in respect to its negation state
				if (lastNegated[layer - 1])
					lastNodes[layer - 1].setZeroChild(lastNodes[layer]);
				else if (!lastNegated[layer - 1])
					lastNodes[layer - 1].setOneChild(lastNodes[layer]);
			}
		}

		else if (exp instanceof Not)
		{
			parseExpression(((Not) exp).getExp());
		}

		else if (exp instanceof True)
		{

			if (lastNegated[layer - 1])
			{
				One newOne = new One();
				lastNodes[layer - 1].setZeroChild(newOne);
				bdd.addNode(newOne);
			}
			else
			{
				One newOne = new One();
				lastNodes[layer - 1].setOneChild(newOne);
				bdd.addNode(newOne);
			}
		}

		else if (exp instanceof False)
		{
			if (lastNegated[layer - 1])
			{
				Zero newZero = new Zero();
				lastNodes[layer - 1].setZeroChild(newZero);
				bdd.addNode(newZero);
			}
			else
			{
				Zero newZero = new Zero();
				lastNodes[layer - 1].setOneChild(newZero);
				bdd.addNode(newZero);
			}
		}

	}

	/**
	 * special handling for shortened boolean expression (e.g. where d.1 is set
	 * to d or d.NOT(d) is set to 0 etc.) the paths to one and zero terminals
	 * are computed here
	 * 
	 * @param exp
	 */
	private void specialHandling(Expression exp)
	{

		if (exp instanceof Variable)
		{
			if (exp.getParent() instanceof And)
			{
				And and = (And) exp.getParent();
				// variable is the right side of an AND expression e.g. c.d
				if (and.getExpressions().get(and.getExpressions().size() - 1) == exp)
				{
					lastNodes[layer].setOneChild(new One());
					lastNodes[layer].setZeroChild(new Zero());
				}
				else if (and.getExpressions().get(0) == exp)
				{
					// variable is the left side of an AND expression and the
					// parent of the AND is not an OR expression e.g. b.c.d
					// where c has no NOT(c) equivalent
					if (!(exp.getParent().getParent() instanceof Or))
					{
						lastNodes[layer].setZeroChild(new Zero());
					}
				}

			}
			else if (exp.getParent() instanceof Not)
			{
				if (exp.getParent().getParent() instanceof And)
				{
					And and = (And) exp.getParent().getParent();
					// //negated variable is the right side of an AND expression
					// e.g. c.d
					if ((and.getExpressions().get(and.getExpressions().size() - 1) == exp.getParent()))
					{
						lastNodes[layer].setZeroChild(new One());
						lastNodes[layer].setOneChild(new Zero());

					}
					else if (and.getExpressions().get(0) == exp)
					{
						// negated variable is the left side of an AND
						// expression and the parent of the AND is not an OR
						// expression e.g. b.c.d
						// where c has no NOT(c) equivalent
						if (!(exp.getParent().getParent().getParent() instanceof Or))
						{
							lastNodes[layer].setOneChild(new Zero());
						}
					}
				}
				else if (exp.getParent() instanceof Or)
				{
					// negated variable is the left side of an OR expression
					// e.g. NOT(b) + b.cd
					if (((Or) exp).getExpressions().get(0) == exp)
					{
						lastNodes[layer].setOneChild(new One());
					}
				}
			}
			else if (exp.getParent() instanceof Or)
			{
				// variable is the left side of an OR expression e.g. NOT(b) +
				// b.cd
				if (((Or) exp.getParent()).getExpressions().get(0) == exp)
				{
					lastNodes[layer].setOneChild(new One());
				}
			}
		}

	}
}
